0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 486 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 348 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 67 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 6 ms)
↳39 QDP
↳40 QDPOrderProof (⇔, 78 ms)
↳41 QDP
↳42 DependencyGraphProof (⇔, 0 ms)
↳43 QDP
↳44 QDPQMonotonicMRRProof (⇔, 77 ms)
↳45 QDP
↳46 QDPQMonotonicMRRProof (⇔, 101 ms)
↳47 QDP
↳48 DependencyGraphProof (⇔, 0 ms)
↳49 TRUE
↳50 PiDP
↳51 UsableRulesProof (⇔, 0 ms)
↳52 PiDP
↳53 PiDPToQDPProof (⇒, 0 ms)
↳54 QDP
↳55 QDPSizeChangeProof (⇔, 0 ms)
↳56 YES
TIMESI_IN_GGA(s(0), X1, X2) → U19_GGA(X1, X2, timescG_in_ga(X1, X3))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → U20_GGA(X1, X2, plusA_in_gga(X1, X3, X2))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → PLUSA_IN_GGA(X1, X3, X2)
PLUSA_IN_GGA(s(X1), X2, s(X3)) → U1_GGA(X1, X2, X3, plusA_in_gga(X1, X2, X3))
PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U21_GGA(X1, X2, X3, evenB_in_ga(X1, X4))
TIMESI_IN_GGA(s(s(X1)), X2, X3) → EVENB_IN_GA(X1, X4)
EVENB_IN_GA(s(s(X1)), X2) → U2_GA(X1, X2, evenB_in_ga(X1, X2))
EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U22_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U23_GGA(X1, X2, X3, halfC_in_ga(X1, X4))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → HALFC_IN_GA(X1, X4)
HALFC_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfC_in_ga(X1, X2))
HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U24_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U25_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U4_GGA(X1, X2, X3, evenB_in_ga(s(X1), X4))
TIMESD_IN_GGA(s(X1), X2, X3) → EVENB_IN_GA(s(X1), X4)
TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U6_GGA(X1, X2, X3, halfC_in_ga(s(X1), X4))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → HALFC_IN_GA(s(X1), X4)
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U8_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U9_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U9_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U10_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U10_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U11_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U12_GGA(X1, X2, X3, plusE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSE_IN_GGA(X5, s(s(s(s(s(s(s(X5))))))), X3)
PLUSE_IN_GGA(s(X1), X2, s(X3)) → U17_GGA(X1, X2, X3, plusE_in_gga(X1, X2, X3))
PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U14_GGA(X1, X2, X3, timesD_in_gga(X1, X2, X4))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U15_GGA(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U16_GGA(X1, X2, X3, plusF_in_gga(X2, X4, X3))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → PLUSF_IN_GGA(X2, X4, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → U18_GGA(X1, X2, X3, plusF_in_gga(X1, X2, X3))
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, s(s(s(s(s(s(s(s(X3))))))))) → U26_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U26_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U27_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U27_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U28_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U29_GGA(X1, X2, X3, plusA_in_gga(X5, s(s(s(s(s(s(s(s(X5)))))))), X3))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSA_IN_GGA(X5, s(s(s(s(s(s(s(s(X5)))))))), X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U30_GGA(X1, X2, X3, evencB_in_gg(X1, false))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U31_GGA(X1, X2, X3, timesD_in_gga(s(X1), X2, X4))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → TIMESD_IN_GGA(s(X1), X2, X4)
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U32_GGA(X1, X2, X3, timescD_in_gga(s(X1), X2, X4))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → U33_GGA(X1, X2, X3, plusA_in_gga(X2, X4, X3))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → PLUSA_IN_GGA(X2, X4, X3)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
TIMESI_IN_GGA(s(0), X1, X2) → U19_GGA(X1, X2, timescG_in_ga(X1, X3))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → U20_GGA(X1, X2, plusA_in_gga(X1, X3, X2))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → PLUSA_IN_GGA(X1, X3, X2)
PLUSA_IN_GGA(s(X1), X2, s(X3)) → U1_GGA(X1, X2, X3, plusA_in_gga(X1, X2, X3))
PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U21_GGA(X1, X2, X3, evenB_in_ga(X1, X4))
TIMESI_IN_GGA(s(s(X1)), X2, X3) → EVENB_IN_GA(X1, X4)
EVENB_IN_GA(s(s(X1)), X2) → U2_GA(X1, X2, evenB_in_ga(X1, X2))
EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U22_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U23_GGA(X1, X2, X3, halfC_in_ga(X1, X4))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → HALFC_IN_GA(X1, X4)
HALFC_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfC_in_ga(X1, X2))
HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U24_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U25_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U4_GGA(X1, X2, X3, evenB_in_ga(s(X1), X4))
TIMESD_IN_GGA(s(X1), X2, X3) → EVENB_IN_GA(s(X1), X4)
TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U6_GGA(X1, X2, X3, halfC_in_ga(s(X1), X4))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → HALFC_IN_GA(s(X1), X4)
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U8_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U9_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U9_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U10_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U10_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U11_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U12_GGA(X1, X2, X3, plusE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSE_IN_GGA(X5, s(s(s(s(s(s(s(X5))))))), X3)
PLUSE_IN_GGA(s(X1), X2, s(X3)) → U17_GGA(X1, X2, X3, plusE_in_gga(X1, X2, X3))
PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U14_GGA(X1, X2, X3, timesD_in_gga(X1, X2, X4))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U15_GGA(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U16_GGA(X1, X2, X3, plusF_in_gga(X2, X4, X3))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → PLUSF_IN_GGA(X2, X4, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → U18_GGA(X1, X2, X3, plusF_in_gga(X1, X2, X3))
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, s(s(s(s(s(s(s(s(X3))))))))) → U26_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U26_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U27_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U27_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U28_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U29_GGA(X1, X2, X3, plusA_in_gga(X5, s(s(s(s(s(s(s(s(X5)))))))), X3))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSA_IN_GGA(X5, s(s(s(s(s(s(s(s(X5)))))))), X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U30_GGA(X1, X2, X3, evencB_in_gg(X1, false))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U31_GGA(X1, X2, X3, timesD_in_gga(s(X1), X2, X4))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → TIMESD_IN_GGA(s(X1), X2, X4)
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U32_GGA(X1, X2, X3, timescD_in_gga(s(X1), X2, X4))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → U33_GGA(X1, X2, X3, plusA_in_gga(X2, X4, X3))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → PLUSA_IN_GGA(X2, X4, X3)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
PLUSF_IN_GGA(s(X1), X2) → PLUSF_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)
PLUSE_IN_GGA(s(X1), X2) → PLUSE_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)
HALFC_IN_GA(s(s(X1))) → HALFC_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)
EVENB_IN_GA(s(s(X1))) → EVENB_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U13_GGA(X1, X2, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMESD_IN_GGA(s(X1), X2) → U13_GGA(X1, X2, evencB_in_gg(s(X1), false))
POL(0) = 0
POL(TIMESD_IN_GGA(x1, x2)) = x1
POL(U13_GGA(x1, x2, x3)) = x1
POL(U36_gg(x1, x2, x3)) = 0
POL(U37_ga(x1, x2)) = 1 + x2
POL(U5_GGA(x1, x2, x3)) = 1 + x1
POL(U7_GGA(x1, x2, x3)) = x3
POL(evencB_in_gg(x1, x2)) = 0
POL(evencB_out_gg(x1, x2)) = 0
POL(false) = 0
POL(halfcC_in_ga(x1)) = x1
POL(halfcC_out_ga(x1, x2)) = x2
POL(s(x1)) = 1 + x1
POL(true) = 0
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
U13_GGA(X1, X2, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
POL(0) = 0
POL(TIMESD_IN_GGA(x1, x2)) = 0
POL(U36_gg(x1, x2, x3)) = x3
POL(U37_ga(x1, x2)) = 0
POL(U5_GGA(x1, x2, x3)) = 2·x3
POL(U7_GGA(x1, x2, x3)) = 0
POL(evencB_in_gg(x1, x2)) = x2
POL(evencB_out_gg(x1, x2)) = 0
POL(false) = 2
POL(halfcC_in_ga(x1)) = 0
POL(halfcC_out_ga(x1, x2)) = 0
POL(s(x1)) = 0
POL(true) = 0
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
POL(0) = 0
POL(TIMESD_IN_GGA(x1, x2)) = 2·x1
POL(U36_gg(x1, x2, x3)) = x2
POL(U37_ga(x1, x2)) = 2 + x2
POL(U5_GGA(x1, x2, x3)) = 2·x1 + 2·x3
POL(U7_GGA(x1, x2, x3)) = 2·x3
POL(evencB_in_gg(x1, x2)) = x2
POL(evencB_out_gg(x1, x2)) = x2
POL(halfcC_in_ga(x1)) = x1
POL(halfcC_out_ga(x1, x2)) = x2
POL(s(x1)) = 2 + x1
POL(true) = 2
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)
PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)
timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)
PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)
PLUSA_IN_GGA(s(X1), X2) → PLUSA_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs: